Inference at * 2 2 
Iof proof for Lemma dcdr-to-bool-equivalence:



1. P : 
2. y : P
3. P
  [inr y ] 

latex

 by (Assert False) 
CollapseTHEN (ProveProp) 

latex

C.

Definitions

False, A, P  Q